We present a PSPACE algorithm that decides satisfiability of the graded modallogic Gr(K_R)---a natural extension of propositional modal logic K_R bycounting expressions---which plays an important role in the area of knowledgerepresentation. The algorithm employs a tableaux approach and is the firstknown algorithm which meets the lower bound for the complexity of the problem.Thus, we exactly fix the complexity of the problem and refute anExpTime-hardness conjecture. We extend the results to the logic Gr(K_(R \capI)), which augments Gr(K_R) with inverse relations and intersection ofaccessibility relations. This establishes a kind of ``theoretical benchmark''that all algorithmic approaches can be measured against.
展开▼
